EN FR
EN FR




Section: Dissemination

Animation of the scientific community

Event organization

  • At the VSTTE 2010 conference was organized a first and informal program verification competition (http://www.macs.hw.ac.uk/vstte10/Competition.html ), as a prelude to more formal competitions in the future. It lasted for 2 hours, and participants had to submit solutions to five simple verification problems. There were 11 participants, and most of them solved only 2 problems.

    On behalf of the VSTTE 2012 conference (Philadelphia, USA, January 2012), A. Paskevich and J.-C. Filliâtre organized the first formal VSTTE program verification competition (https://sites.google.com/site/vstte2012/compet ). This time it lasted for 48 hours, from November 8 to November 10. A set of five verification problems was proposed to the participants. The problems to solve were significantly harder than those of 2010. Each problem consisted of an algorithm given in pseudocode, together with a set of properties to be mechanically proved. A total of 29 teams (79 participants) sent solutions, which is considered an excellent success. These solutions are currently under examination. Results will be announced at the conference.

Editorial boards

  • S. Boldo is member of the editorial committee of the popular science web site interstices, http://interstices.info/ .

  • J.-C. Filliâtre is member of the editorial board of the Journal of Functional Programming.

  • C. Marché co-edited with B. Beckert a special issue of Elsevier Lectures Notes in Computer Science devoted to selected papers of the conference FoVeOOS'10 [34] .

  • C. Paulin is member of the editorial board of the Journal of Formalized Reasoning.

  • J.-C. Filliâtre edited a special issue of Software Tools for Technology Transfer devoted to selected papers of the workshop VSTTE 2009. This includes an introduction paper on deductive software verification [18] .

Learned societies

  • J.-C. Filliâtre is a member of IFIP Working Group 1.9/2.15 (Verified Software)

Program committees

  • S. Conchon, program chair of the Journées Francophones des Langages Applicatifs (JFLA 2011), La Bresse, France, January 2011.

  • S. Boldo, member of the program committee of JFLA 2011, and the Fourth International Workshop on Numerical Software Verification (NSV 2011, affiliated to CAV).

  • D. Baelde, G. Melquiond, members of the program committee of JFLA 2012.

  • É. Contejean is a member of program committees of the ACM SIGPLAN 2011 Workshop on Partial Evaluation and Program Manipulation (PEPM 2011, co-located with POPL, Austin, Texas), the International Workshop on Proof Search in Axiomatic Theories and Type Theories (PSATTT 20011, affiliated to CADE, Wroclaw, Poland).

  • C. Marché, member of program committees of the 2nd International Conference on Formal Verification of Object-Oriented Software (FoVeOOS 2011, Turin, Italy), the 23rd International Conference on Automated Deduction (CADE 2011, Wroclaw, Poland), and the the first International Workshop on Intermediate Verification Languages (BOOGIE 2011, affiliated to CADE).

  • C. Paulin, member of the program committee of the second and third conference on Interactive Theorem Proving (ITP 2011 & 2012), and the Fifth ACM SIGPLAN Workshop on Programming Languages meets Program Verification (PLPV 2011), affiliated to POPL.

  • J.-C. Filliâtre, member of the program committee of the second conference on Interactive Theorem Proving (ITP 2011), the workshop “Analyze to Compile, Compile to Analyze” (ACCA 2011), and the conference Verified Software: Theories, Tools and Experiments (VSTTE 2012).

Participation to Thesis Committees

  • C. Marché: president of PhD committee of Diego Caminha Barbosa de Oliveira (University Nancy 2, March 14th, 2011)

  • C. Marché: reviewer, PhD of Beatriz Alarcón (University of Valencia, Spain, May 26th, 2011)

  • C. Marché: reviewer, PhD of Mauricio Alba Castro (University of Valencia, Spain, Nov 25th, 2011)

  • C. Marché: reviewer, PhD of Séverine Maingaud (University Paris 7, Dec 13th, 2011)

  • C. Paulin: examinator, PhD of Mathias Krieger (University Paris-Sud 11, Dec 9th, 2011)

Invited Presentations

  • S. Boldo, “Contours de la communauté”, invited talk at the 4es Rencontres Arithmétique de l'Informatique Mathématique (RAIM'11) in Perpignan. (Collected data about the outline of the computer arithmetic community in France: sites, themes, fundings...).

  • J.-C. Filliâtre, “Memo Tables”, invited at the IFIP Working Group 2.8 Functional Programming (Marble Falls, Texas, USA, March 7–11, 2011).

  • P. Herms, “Certification of a Verification Condition Generator in Coq”, seminar of the Gallium-Moscova teams, Rocquencourt, June 20th.

  • C. Marché, “Verifying Behavioral Specifications of Programs: the Why Approach”, seminar of the ELP team, Departamento de Sistemas Informáticos y Computación, Universidad Politécnica de Valencia, Spain, March 25th.

  • T. Nguyen, “Hardware-independent proofs of numerical programs ”, seminar of the Arenaire team, Lyon, January 20th.

  • C. Paulin, “About Inductive-Recursive Definitions in Coq”, invited speaker at the workshop on Proofs and Programs, Gothenburg, Sweden, Oct. 22th.